#include "VSIDS.cuh"

__device__ VSIDS::VSIDS(int number_of_variables):
	decay_factor(2),
	clauses_before_decaying(50),
	random_decision_frequency(0.01)

{
	this->number_of_variables = number_of_variables;
	this->number_of_decisions = 0;
	this->number_of_learnt_clauses = 0;
	variables = (vsids_variable*) malloc(number_of_variables*sizeof(vsids_variable));

	for(int i = 0;i < number_of_variables; i++)
	{
		variables[i].free = true;
		variables[i].negative_lit_sum = 0;
		variables[i].positive_lit_sum = 0;
	}

	unsigned long seed = (unsigned long) clock();

	initCurand(seed);

}

__device__ void VSIDS::initCurand(unsigned long seed){
    curand_init(seed, 0, 0, &randState);
}

__device__ Var VSIDS::next_random_var()
{
	Var v;

	do
	{
		unsigned int int_value = curand(&randState);
		v = int_value % number_of_variables;
	}
	while(!variables[v].free);


	return v;
}
__device__ bool VSIDS::next_random_polarity()
{
	unsigned int int_value = curand(&randState);
	bool polarity = int_value % 2 == 0 ? true : false;

	return polarity;
}

__device__ void VSIDS::decay()
{
	for(int i = 0;i < number_of_variables; i++)
	{
		variables[i].negative_lit_sum /= decay_factor;
		variables[i].positive_lit_sum /= decay_factor;
	}
}

__device__ void VSIDS::increment(Lit literal)
{
	Var variable = var(literal);
	bool s = sign(literal);

	if(s)
		variables[variable].positive_lit_sum++;
	else
		variables[variable].negative_lit_sum++;

}

__device__ void VSIDS::free_variable(Var v)
{
#ifdef USE_ASSERTIONS
	assert(v >= 0 && v < number_of_variables);
#endif
	variables[v].free = true;
}

__device__ void VSIDS::block_variable(Var v)
{
#ifdef USE_ASSERTIONS
	assert(v >= 0 && v < number_of_variables);
#endif
	variables[v].free = false;
}

__device__ void VSIDS::handle_clause(Clause c)
{
	for(int i = 0; i < c.number_of_lits; i++)
	{
		Lit literal = c.literals[i];
		increment(literal);
	}

	number_of_learnt_clauses++;

	if(number_of_learnt_clauses % clauses_before_decaying == 0
			&& number_of_learnt_clauses > 0)
		decay();

}

__device__ Lit VSIDS::next_random_literal()
{
	Var v = next_random_var();

	bool polarity = next_random_polarity();

	Lit l = mkLit(v, polarity);

	return l;

}

__device__ Lit VSIDS::next_higher_literal()
{

	Lit higher;
	higher.x = -1;

	int last_sum = -1;

	for(int i = 0; i < number_of_variables; i++)
	{
		vsids_variable vvar = variables[i];

		if(vvar.free)
		{
			if(vvar.positive_lit_sum > last_sum)
			{
				Lit l = mkLit(i, true);
				last_sum = vvar.positive_lit_sum;
				higher = l;
			}
			if(vvar.negative_lit_sum > last_sum)
			{
				Lit l = mkLit(i, false);
				last_sum = vvar.negative_lit_sum;
				higher = l;
			}

		}

	}
#ifdef USE_ASSERTIONS
	assert(higher.x >= 0);
#endif

	return higher;

}

__device__ Lit VSIDS::next_literal()
{
	float prop = curand_uniform(&randState);

	if(prop < random_decision_frequency)
	{
		return next_random_literal();
	}

	//if(number_of_decisions % clauses_before_decaying == 0 && number_of_decisions > 0)
	//	decay();

	number_of_decisions++;

	return next_higher_literal();

}
__device__ bool VSIDS::is_free(Var v)
{
	return variables[v].free;
}

__device__ void VSIDS::print()
{
	printf("Evals[%d] = {", number_of_variables);
	for(int i = 0; i < number_of_variables; i++)
	{
		Lit lp = mkLit(i, true);
		Lit ln = mkLit(i, false);

		print_lit(lp);
		printf("=%d ", variables[i].positive_lit_sum);
		print_lit(ln);
		printf("=%d(%s), ", variables[i].negative_lit_sum, variables[i].free ? "T" : "F");

	}
	printf("}\nDecisions = %d\n", number_of_decisions);


}
